\begin{tabbing}
$\forall$${\it es}$:ES, $e$:E.
\\[0ex]($\neg$($\uparrow$first($e$)))
\\[0ex]$\Rightarrow$ (\=(timed)state after pred($e$)+time($e$) {-} time(pred($e$))\+
\\[0ex]=
\\[0ex]es\_state\_when(${\it es}$;$e$)
\\[0ex]$\in$ es\_state(${\it es}$;loc($e$)))
\-
\end{tabbing}